Nuprl Lemma : comb_for_int_upper_wf
9,38
postcript
pdf
(
n
,
z
. {
n
...})
(
True)
Type
latex
ProofTree
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
true
wf
,
squash
wf
,
int
upper
wf
origin
n,z. {n...}) 
(
True)Type
n,z. {n...}) (True)Type
T
x:A. B(x)T